Nuprl Lemma : star-append_wf
0,22
postcript
pdf
T
:Type,
P
,
Q
:((
T
List)
Prop). star-append(
T
;
P
;
Q
)
(
T
List)
Prop
latex
Definitions
t
T
,
Prop
,
x
:
A
.
B
(
x
)
,
concat(
ll
)
,
as
@
bs
,
P
&
Q
,
x
.
t
(
x
)
,
x
L
.
P
(
x
)
,
x
:
A
.
B
(
x
)
,
star-append(
T
;
P
;
Q
)
Lemmas
l
all
wf
,
append
wf
,
concat
wf
origin
T:Type, P, Q:((T List)
Prop). star-append(T;P;Q) 
(T List)Prop T:Type, P, Q:((T List)Prop). star-append(T;P;Q) (T List)Prop Tx:A. B(x)
x. t(x)xL. P(x)
x:A. B(x)